Step of Proof: multiply_nat_wf 12,41
Inference at * 2 0 1 3 1 2 
Iof proof for Lemma multiply nat wf:



1. i : 
2. j : 
3. 0 < j
4. 0  (i * (j - 1))
  0  (i * j) 
latex
 by AddHiddenLabel `upcase` 
latex

 1: .....upcase..... NILNIL

 1:   0  (i * j)
 .

origin